the_es:ES, e:E, l:IdLnk. rcvs(l;before(e))  ({e:E| haslnk(l;e)}  List) 

latex

Definitions	x:A. B(x), t  T, P  Q, T, True, , i  j , A  B, A, False, , rcvs(l;before(e')), filter(P;l), before(e), Y, if b then t else f fi , tt, reduce(f;k;as), ff, SWellFounded(R(x;y)), x:A. B(x), , Unit, P  Q, P & Q,
Lemmas	es-locl-swellfnd, nat wf, es-E wf, event system wf, le wf, es-locl wf, nat properties, ge wf, es-first wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, IdLnk wf, es-haslnk wf, filter append, es-before wf, es-pred wf, es-pred-locl, append wf